Hm, I need to figure out where the what4-solvers binaries are actually located on the awslc job. Currently, that job fails with:

+ rm bin/saw
+ cp /saw-bin/saw bin/saw
+ cp /saw-bin/abc bin/abc
+ cp /saw-bin/z3-4.8.10 bin/z3
cp: cannot stat '/saw-bin/z3-4.8.10': No such file or directory
1
make: *** [Makefile:25: awslc] Error 1

(cp /saw-bin/z3-4.8.10 bin/z3 was an educated guess, but an incorrect one.)

Ah, this is because I hadn't changed .github/ci.sh to actually copy over z3-4.8.10 into the uploaded artifact. After doing that, the AWSLC proofs now use z3-4.8.10, and the result is:

[15:10:02.875] Checking proof obligations ECDSA_do_verify ...
Killed
137
make: *** [Makefile:25: awslc] Error 137
Error: Process completed with exit code 2.

Ugh.

I realized something while looking at the entrypoint script for AWSLC:

Namely, this was never copying over the what4-solvers version of Z3 in the first place! It copies over the what4-solvers version of abc (which lives under /saw-bin) to /bin (which is what is put onto the PATH), but no other solver receives this treatment. The remaining solvers come from the install.sh script, which lives in the aws-lc-verification repo:

Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip'

# ...

# fetch Z3
if [ ! -f bin/z3 ]
then
    mkdir -p deps/z3
    wget $Z3_URL -O deps/z3.zip
    unzip deps/z3.zip -d deps/z3
    cp deps/z3/*/bin/z3 bin/z3
fi

This is a double whammy: not only was the AWSLC script installing a different version of Z3 than we originally expected (4.8.8), it was installing the Ubuntu 16.04 version! It is a minor miracle that this continued to work for as long as it did.

Unfortunately, this PR has demonstrated that using the Ubuntu 22.04 version of Z3 4.8.10 with the AWSLC proofs results in the OOM killer acting up. On the other hand, we have never actually tried the Ubuntu 22.04 version of Z3 4.8.14, so I will push a change that tries out 4.8.14 on the AWSLC proofs.

While I was in town, I noticed that the BLST entrypoint script is somewhat overwrought:

This re-downloads the what4-solvers binaries, but there is no point in doing so, as they are already available under /bin. I will push a separate commit to simplify this.

Sadly, the OOM killer still activates on the AWSLC proofs even with Z3 4.8.14. I suppose we could try using Z3 4.8.8 next, as that is the Z3 version that is used in aws-lc-verifications's install.sh script.

Well, the AWSLC/BLST proofs passed after downgrading to Z3 4.8.8. Let's see if this is consistent after restarting those jobs a couple of times...

With Z3 4.8.8, the AWSLC and BLST jobs have succeeded on three consecutive runs, which makes me cautiously optimistic. I've rebased everything, and assuming that this successful CI trend continues after this rebase, then I'm declaring victory.

Hot dog, I think it works! @chameco, does everything look good to you?

@Mergifyio refresh

refresh

✅ Pull request refreshed